//      // verilator_coverage annotation
        module counter_props (
 000203     input wire clk,
%000001     input wire rst_n,
 000027     input wire en,
~000050     input wire [3:0] cnt,
%000006     input wire ovf
        );
            //初始强制复位
%000001     initial assume(!rst_n);
            // ==============================================
            // 断言1: 复位生效后计数器必须归零且无溢出
            // 原始SVA: !rst_n |=> (cnt == 0 && !ovf)
            // ==============================================
 000102     always @(posedge clk) begin
~000101         if (!rst_n) begin
%000001             assert (cnt == 4'b0 && ovf == 1'b0);
                end
            end
            // ==============================================
            // 断言2: 使能有效时计数器必须自动递增
            // 原始SVA: en && (cnt < 4'hf) |=> cnt == past_cnt + 1
            // ==============================================
 000102     always @(posedge clk) begin
~000056         if (rst_n && $past(rst_n)  && $past(en) && ($past(cnt) < 4'hf) ) begin
                    // 检查下一个周期的值
 000046             assert (cnt == ($past(cnt) + 1));
                end
                // 错误状态保持一个周期
            end
            // ==============================================
            // 断言3: 计数器满后必须归零并置位溢出
            // 原始SVA: en && (past_cnt == 4'hf) |=> (cnt == 0 && ovf)
            // ==============================================
 000102     always @(posedge clk) begin
~000101         if ($past(rst_n)&& rst_n && $past(en)&& en && ($past(cnt) == 4'hf)) begin
%000001             assert (cnt == 4'b0 && ovf == 1'b1);
                end
            end
            // ==============================================
            // 覆盖率收集（保持原功能）
            // ==============================================
            generate
%000000         for (genvar i = 0; i < 16; i++) begin : gen_covers
 001632             always @(posedge clk) begin
%000000                 cover (cnt == i);
                    end
                end
            endgenerate
        //    always @(posedge clk) begin
        //        cover (cnt == 16);
        //    end
        endmodule
